$\forall$$i$:Id, $l$:IdLnk, ${\it da}$:fpf(Knd; $k$.Type), ${\it tg}$:Id, $k$:Knd, $n$,$f$:top.
\\[0ex]msg{-}spec{-}loc{-}decl(msg{-}spec1($k$; $l$; ${\it tg}$; $n$; $s$,$v$.$f$($s$,$v$)); $i$; ${\it da}$)
\\[0ex]$\Leftarrow\!\Rightarrow$ ((source($l$) = $i$) $\wedge$ ($\uparrow$fpf{-}dom(Kind{-}deq; rcv($l$,${\it tg}$); ${\it da}$)))